@inproceedings{Coppo:1978,
 author = {Coppo, Mario and Dezani-Ciancaglini, Mariangiola and Rocca, Simona Ronchi Della},
 title = {(Semi)-separability of Finite Sets of Terms in Scott's $\mathrm{D}_{\infty}$-Models of the lambda-Calculus},
 booktitle = {Proceedings of the Fifth Colloquium on Automata, Languages and Programming},
 year = {1978},
 isbn = {3-540-08860-1},
 pages = {142--164},
 numpages = {23},
 url = {http://dl.acm.org/citation.cfm?id=646232.682078},
 acmid = {682078},
 publisher = {Springer-Verlag},
 address = {London, UK, UK},
} 

@book{whitehead1927principia,
  title={Principia mathematica. 2.1927},
  author={Whitehead, A.N. and Russell, B.},
  lccn={lc25015133},
  series={Principia Mathematica},
  url={http://books.google.com/books?id=JCMgAQAAIAAJ},
  year={1927},
  publisher={Cambridge University Press}
}
@book{Barendregt:1985,
  title={The lambda calculus: Its syntax and semantics},
  author={Barendregt, Hendrik Pieter},
  volume={103},
  year={1985},
  publisher={North Holland}
}
@article{zermelo1908untersuchungen,
  title={Untersuchungen {\"u}ber die Grundlagen der Mengenlehre. I},
  author={Zermelo, Ernst},
  journal={Mathematische Annalen},
  volume={65},
  number={2},
  pages={261--281},
  year={1908},
  publisher={Springer}
}

@article{quine1937new,
  title={New foundations for mathematical logic},
  author={Quine, Willard V},
  journal={The American mathematical monthly},
  volume={44},
  number={2},
  pages={70--80},
  year={1937},
  publisher={JSTOR}
}
@book{Girard:1989,
 author = {Girard, Jean-Yves and Taylor, Paul and Lafont, Yves},
 title = {Proofs and types},
 year = {1989},
 isbn = {0-521-37181-3},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
} 
@incollection{Bove:2009,
  title={A brief overview of Agda--a functional language with dependent types},
  author={Bove, Ana and Dybjer, Peter and Norell, Ulf},
  booktitle={Theorem Proving in Higher Order Logics},
  pages={73--78},
  year={2009},
  publisher={Springer}
}

@article{Coq,
  title={The Coq Proof Assistant Reference Manual},
  author={The Coq Development Team},
  journal={Version 8.3. INRIA},
  publisher={Available from http://coq.inria.fr/V8.3/refman/},
  year={2010}
}

@book{takeuti1975proof,
  title={Proof Theory},
  author={Takeuti, G.},
  lccn={75023164},
  series={Volume 81 of Studies in logic and the foundations of mathematics, ISSN 0049-237X},
  url={http://books.google.com/books?id=tMSEAAAAIAAJ},
  year={1975},
  publisher={North-Holland Publishing Company}
}


@article{leroy1998ocaml,
  title={The OCaml programming language},
  author={Leroy, Xavier},
  journal={Online},
  url={http://caml. inria. fr/ocaml/index.en.html},
  year={1998}
}

@book{jones2003haskell,
  title={Haskell 98 language and libraries: the revised report},
  author={Jones, Simon L Peyton},
  year={2003},
  publisher={Cambridge University Press}
}

@book{Church:1985,
 author = {Church, Alonzo},
 title = {The Calculi of Lambda Conversion. (AM-6) (Annals of Mathematics Studies)},
 year = {1985},
 isbn = {0691083940},
 publisher = {Princeton University Press},
 address = {Princeton, NJ, USA},
}

@book{CHS:72,
  author = {H. B. Curry and J. R. Hindley and J. P. Seldin},
  title = {Combinatory Logic, Volume II},
  publisher = {North-Holland},
  year = {1972},
  pages = {xiv+520}
}

@phdthesis{vaninwegen1996machine,
  title={The machine-assisted proof of programming language properties},
  author={VanInwegen, Myra},
  year={1996},
  school={University of Pennsylvania}
}

@inproceedings{parigot1988programming,
  title={Programming with proofs: a second order type theory},
  author={Parigot, Michel},
  booktitle={ESOP'88},
  pages={145--159},
  year={1988},
  organization={Springer}
}

@book{Winskel:1993,
 author = {Winskel, Glynn},
 title = {The formal semantics of programming languages: an introduction},
 year = {1993},
 isbn = {0-262-23169-7},
 publisher = {MIT Press},
 address = {Cambridge, MA, USA},
} 
@phdthesis{Raffalli:1994,
  title={L' Arithm\'etiques Fonctionnelle du Second Ordre avec Points Fixes},
  author={Christophe RAFFALLI},
  year={1994},
  school={L'universit\'e Paris VII}
}

@book{matthes1999extensions,
  title={Extensions of system F by iteration and primitive recursion on monotone inductive types},
  author={Matthes, Ralph},
  year={1999},
  publisher={Herbert Utz Verlag}
}

@inproceedings{fu2011framework,
  title={A Framework for Internalizing Relations into Type Theory},
  author={Fu, Peng and Stump, Aaron and Vaughan, Jeffrey},
  booktitle={PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories},
  year={2011}
}

@article{krivine2002lambda,
  title={Lambda-calculus types and models},
  author={Krivine, Jean-Louis},
  year={2002}
}

@misc{frege1967basic,
  title={The Basic Laws of Arithmetic: Exposition of the System, translated and edited with an introduction by Montgomery Furth},
  author={Frege, Gottlob},
  year={1967},
  publisher={University of California Press}
}
@book{hatcher:1982,
  title={The logical foundations of mathematics},
  author={Hatcher, William S},
  volume={10},
  year={1982},
  publisher={Pergamon Press Oxford}
}

@inproceedings{leivant1983reasoning,
  title={Reasoning about functional programs and complexity classes associated with type disciplines},
  author={Leivant, Daniel},
  booktitle={Foundations of Computer Science, 1983., 24th Annual Symposium on},
  pages={460--469},
  year={1983},
  organization={IEEE}
}

@INPROCEEDINGS{Barendregt:92,
    author = {Henk Barendregt and S. Abramsky and D. M. Gabbay and T. S. E. Maibaum and H. P. Barendregt},
    title = {Lambda Calculi with Types},
    booktitle = {Handbook of Logic in Computer Science},
    year = {1992},
    pages = {117--309},
    publisher = {Oxford University Press}
}
